Hand-writing a Clara-compatible monitor
If you know how to write AspectJ aspects, you can easily write Clara-compatible runtime monitors yourself, in three simple steps.
1. Write the aspect as you normally would
There are no special constraints. You can use any AspectJ features you like. (Note though, that our implementation is based on abc, which does not yet support AspectJ 5. However, you can use Clara to weave into Java 5 Programs.) The following example shows a hand-written monitoring aspect for the “ConnectionClosed” property. This property states that one should not write to a connection that has been closed.
aspect ConnectionClosed { Set closed = new WeakIdentityHashSet(); after(Connection c) returning: call(* Connection.close()) && target(c) { closed.add(c); } after(Connection c) returning: call(* Connection.reconnect()) && target(c) { closed.remove(c); } after(Connection c) returning: call(* Connection.write(..)) && target(c) { if(closed.contains(c)) error("May not write to "+c+", as it is closed!"); } }
2. Declare pieces of advice as “dependent” and assign them names
Next, declare all appropriate pieces of advice as dependent, and assign some meaningful names to these pieces of advice:
aspect ConnectionClosed { ... after close(Connection c) returning: ... } after reconnect(Connection c) returning: ... } after write(Connection c) returning: ... } ... }
3. Add dependency annotation
Next, we need to add the appropriate dependency annotation. This is the only part that may become somewhat tricky. When you do not generate your monitor from a high-level specification, then you as a programmer have to determine the exact transition structure that your runtime monitor has. For the above example, we can find the following:
- We start in an initial state in which it is ok to write to the connection. The set closed does not yet contain the connection.
- Closing the connection brings us into a state in which it is not ok to write to the connection. The connection is in the set closed.
- From there, we can either…
- reconnect the connection, which removes the connection from the set again and thus moves the connection back to the initial state, or
- write to the connection, which triggers an error.
- When being in the error state, then another write will show the error message again.
The figure on the right-hand side shows one possible state machine to model this transition structure. In general, any equivalent state machine that accepts the same regular language will do. Clara does not care about which particular state machine you use and whether it’s deterministic or not.
All you then have to do is just encode this state machine in a textual format:
dependency{ close, write, reconnect; initial connected: close -> connected, write -> connected, reconnect -> connected, close -> closed; closed: close -> closed, write -> error; final error: write -> error; }
Simple enough, isn’t it? Line 2 simply lists all “symbols” in the alphabet that the state machine operates one. The following lines then encode the transition table.
Note that line2, closed, write, reconnect does not mention the name of the connection c. This is because, by default, Clara infers these names from the variable names that are declared in the respective pieces of advice. In the example, closed, write, reconnect is thus a short-hand for closed(c), write(c), reconnect(c). This short-hand version is fine as long as all pieces of advice refer to the connection using the same variable name c. If they don’t, then the user has to state the variable names explicitly in the dependency declaration. For instance, the following would be an equivalent aspect where variable names differ but where the dependency declaration “unifies” these names using one and the same variable name c in all positions (line 3).
aspect ConnectionClosed { dependency{ close(c), write(c), reconnect(c); initial connected: close -> connected, write -> connected, reconnect -> connected, close -> closed; closed: close -> closed, write -> error; final error: write -> error; } Set closed = new WeakIdentityHashSet(); after(Connection c1) returning: call(* Connection.close()) && target(c1) { closed.add(c1); } after(Connection c2) returning: call(* Connection.reconnect()) && target(c2) { closed.remove(c2); } after(Connection c3) returning: call(* Connection.write(..)) && target(c3) { if(closed.contains(c3)) error("May not write to "+c3+", as it is closed!"); } }
Because we use the same variable name c in all positions in the dependency, Clara “knows” that all three pieces of advice are meant to refer to the same connection object.